COMMENT ⊗   VALID 00013 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(wipe-out)
C00004 00003	PROOFS
C00005 00004	(proof pigeonfacts)
C00015 00005	(proof uniqueness_alist)
C00016 00006	(proof invimage_lemmata)
C00018 00007	nth range
C00022 00008	nth dom:
C00026 00009	(proof nthcdr_dom)
C00028 00010	(proof member_memberdom)
C00031 00011	(proof invimage)
C00039 00012
C00050 00013
C00053 ENDMK
C⊗;
(wipe-out)
(get-proofs pigeon prf ekl sys)

;(label dijpair_def sums#10)
;(label disjointdef sums#12)

(proof alistfacts)

(axiom |∀alist.length (dom(alist))=length alist|)
(label domlength)

(define invimage |∀n alist.invimage(n,alist)=
                           (λxv.atom xv∧∃y.member(xv.y,alist)∧(setseq(n))(y))|)

(axiom |∀chi3.(∀alist n xa y.chi3(nil,n)∧chi3(alist,0)∧
                             (chi3(alist,n)⊃chi3((xa.y).alist,n')))⊃
              (∀alist n.chi3(alist,n))|)
(label double_alistinduction1)

(axiom |∀alist n.n<length dom(alist)⊃atom(nth(dom alist,n))|)
(label atom_nth)

(axiom |∀alist n.uniqueness(dom(alist))∧n<length (dom(alist))⊃
                 appalist(nth(dom(alist),n),alist)=nth(range(alist),n)|)
(label appalist_nth)
;PROOFS
(proof pigeonfacts)

(axiom |∀x u.alistp(x.u)⊃¬atom x∧atom car x∧alistp u|)
(label alistfact1)

(axiom |∀x u.alistp(x.u)⊃alistp u|)
(label alistfact2)

(axiom |∀u n.alistp u⊃alistp nthcdr(u,n)|)
(label alist_nthcdr)

(axiom |∀u n.alistp u∧n<length u⊃¬atom nth(u,n)∧atom car nth(u,n)|)
(label nthalist_sort)

(axiom |∀u n.alistp u∧n<length u⊃cdr nth(u,n)=nth(range(u),n)|)
(label nth_range)

(axiom |∀u n.alistp u∧n<length u⊃car nth(u,n)=nth(dom(u),n)|)
(label nth_dom)

(axiom |∀setseq n.un(λm.setseq(m),n)=(λx.∃k.k<n∧(setseq k)(x))|)
(label unionfact2)

(axiom |∀alist x y.cdr assoc(x,alist)=y⊃assoc(x,alist)=x.y|)
(label assocfact1)

(axiom |∀u n.alistp u⊃nthcdr(dom(u),n)=dom(nthcdr(u,n))|)
(label nthcdr_dom)

(axiom |∀alist xa1 y1.member(xa1.y1,alist)⊃member(xa1,dom(alist))|)
(label member_memberdom)

;theorem 
(axiom |(∀n.n<length alist⊃disjoint(λm.setseq(m),n'))∧
        inj(dom(alist))⊃
        (∀n.n≤length alist⊃disjoint(λm.invimage(m,alist),n))|)
(label disjoint_invimage)
(proof uniqueness_alist)

(trw |∀x y.x=y⊃car(x)=car(y)|)
;∀X Y.X=Y⊃CAR X=CAR Y

(ue ((x.|xa.y|)(y.|xa1.y1|)) *)
;XA.Y=XA1.Y1⊃XA=XA1

(ue (chi |λalist.member(xa.y,alist)⊃member(xa,dom alist)|) alistinduction
    (open member dom) (use normal * mode: always))
;∀ALIST.MEMBER(XA.Y,ALIST)⊃MEMBER(XA,DOM(ALIST))

(derive |∀alist xa y.¬member(xa,dom(alist))⊃¬member(xa.y,alist)| *)

(ue (chi |λalist.uniqueness dom(alist)⊃uniqueness alist|) alistinduction
    (open dom uniqueness member) *)
;∀ALIST.UNIQUENESS(DOM(ALIST))⊃UNIQUENESS(ALIST)
(label uniqueness_dom_alist)

(proof invimage_lemmata)
;uniqueness nthcdr

(ue (phi3 |λu n.uniqueness u⊃uniqueness nthcdr(u,n)|) doubleinduction1 
    (open uniqueness nthcdr))
;∀U N.UNIQUENESS(U)⊃UNIQUENESS(NTHCDR(U,N))
(label uniqueness_nthcdr)

;alistp nthcdr

(ue (phi3 |λu n.alistp u⊃alistp nthcdr(u,n)|) doubleinduction1 alistfact2)
;∀U N.ALISTP U⊃ALISTP NTHCDR(U,N)
(label alistp_nthcdr)

;nthalist sort

(ue (phi |λu.alistp u∧0<length u⊃¬atom car u∧atom car (car u)|) 
    listinduction alistfact1)
;∀U.ALISTP U∧0<LENGTH U⊃¬ATOM CAR U∧ATOM CAR (CAR U)

(ue (phi3 |λu n.alistp u∧n<length u⊃¬atom nth(u,n)∧atom car nth(u,n)|) 
    doubleinduction1 alistfact1 *)
;∀U N.ALISTP U∧N<LENGTH U⊃¬ATOM NTH(U,N)∧ATOM CAR NTH(U,N)
(label nthalist_sort)

;nth range

(ue (phi3 |λu n.n<length u∧alistp u⊃cdr nth(u,n)=nth(range(u),n)|) 
    doubleinduction1 alistfact1 nthalist_sort (open range))
(ue (phi |λu.(0<LENGTH U∧ALISTP U⊃CDR (CAR U)=CAR RANGE(U))|) 
    listinduction alistfact1 (open range))
;(∀X U.(0<LENGTH U∧ALISTP U⊃CDR (CAR U)=CAR RANGE(U))⊃
;      (ALISTP X.U⊃CDR X=CAR RANGE(X.U)))⊃
;(∀U.0<LENGTH U∧ALISTP U⊃CDR (CAR U)=CAR RANGE(U))

(assume |0<length u|)
(label invil1)

(assume |alistp u|)
(label invil2)

(trw |sexp car(u)| invil1)
;SEXP CAR U
(label invil3)

(ue((x.|car u|)(u.|cdr u|)) alistfact1 invil1 invil2 *)
;¬ATOM CAR U∧ATOM CAR (CAR U)∧ALISTP CDR U
(label invil4)
;deps: (INVIL1 INVIL2)

(trw |car (range (((car car u).cdr car u).cdr u))|
     (nuse cons_car_cdr) (open range) invil1 invil3 *)
;CAR RANGE((CAR (CAR U).CDR (CAR U)).CDR U)=CDR (CAR U)
;deps: (INVIL1 INVIL2)

(trw |(car car(u)).(cdr car(u))| invil4)
;CAR (CAR U).CDR (CAR U)=CAR U
;deps: (INVIL1 INVIL2)

(rw -2 (use * mode: exact) invil1)
;CAR RANGE(U)=CDR (CAR U)
;deps: (INVIL1 INVIL2)

(ci (invil1 invil2))
;0<LENGTH U∧ALISTP U⊃CAR RANGE(U)=CDR (CAR U)
(label invil_basecase)

(assume |n<length u∧alistp u⊃cdr nth(u,n)=nth(range(u),n)|) 
(label invil5)

(assume |n'<length(x.u)∧alistp x.u|)
(label invil6)

(rw *)
;N<LENGTH U∧ALISTP X.U

(derive |cdr nth(u,n)=nth(range(u),n)| (* alistfact2 invil5))
(label invil7)

(derive |¬atom x∧atom car x∧alistp u| (invil6 alistfact1))

(trw |nth(range((car x.cdr x).u),n')| (nuse cons_car_cdr) (open range) *)
;NTH(RANGE((CAR X.CDR X).U),N')=NTH(RANGE(U),N)
;deps: (INVIL6)

(rw invil7 (use * mode: exact direction: reverse))
;CDR NTH(U,N)=NTH(RANGE((CAR X.CDR X).U),N')
;deps: (INVIL5 INVIL6)

(trw |car x.cdr x| -3)
;CAR X.CDR X=X
;deps: (INVIL6)

(rw -2 *)
;CDR NTH(U,N)=NTH(RANGE(X.U),N')
;deps: (INVIL5 INVIL6)

(ci invil6)
;N<LENGTH U∧ALISTP X.U⊃CDR NTH(U,N)=NTH(RANGE(X.U),N')
;deps: (INVIL5)

(ci invil5)
;(N<LENGTH U∧ALISTP U⊃CDR NTH(U,N)=NTH(RANGE(U),N))⊃
;(N<LENGTH U∧ALISTP X.U⊃CDR NTH(U,N)=NTH(RANGE(X.U),N'))
(label invil_inductioncase)

(ue (phi3 |λu n.n<length u∧alistp u⊃cdr nth(u,n)=nth(range(u),n)|) 
    doubleinduction1 invil_basecase invil_inductioncase)
;∀U N.N<LENGTH U∧ALISTP U⊃CDR NTH(U,N)=NTH(RANGE(U),N)

;nth dom:
;similarly
(proof nthdom)

(axiom |∀u n.alistp u⊃cdr nth(u,n)=nth(range(u),n)|)
(label invimage_l1)

(ue (phi3 |λu n.n<length u∧alistp u⊃cdr nth(u,n)=nth(range(u),n)|) 
    doubleinduction1 alistfact1 nthalist_sort (open range))
(ue (phi |λu.alistp u∧0<length u⊃car (car u)=car dom(u)|) 
    listinduction alistfact1 (open dom))
;(∀X U.(ALISTP U∧0<LENGTH U⊃CAR (CAR U)=CAR DOM(U))⊃
;      (ALISTP X.U⊃CAR X=CAR DOM(X.U)))⊃
;(∀U.ALISTP U∧0<LENGTH U⊃CAR (CAR U)=CAR DOM(U))

(ekl)
;(∀X U.(0<LENGTH U∧ALISTP U⊃CDR (CAR U)=CAR RANGE(U))⊃
;      (ALISTP X.U⊃CDR X=CAR RANGE(X.U)))⊃
;(∀U.0<LENGTH U∧ALISTP U⊃CDR (CAR U)=CAR RANGE(U))

(assume |0<length u|)
(label nthd1)

(assume |alistp u|)
(label nthd2)

(trw |sexp car(u)| nthd1)
;SEXP CAR U
(label nthd3)

(ue((x.|car u|)(u.|cdr u|)) alistfact1 nthd1 nthd2 *)
;¬ATOM CAR U∧ATOM CAR (CAR U)∧ALISTP CDR U
(label nthd4)

(trw |car (dom (((car car u).cdr car u).cdr u))|
     (nuse cons_car_cdr) (open dom) nthd1 nthd3 *)
;CAR DOM((CAR (CAR U).CDR (CAR U)).CDR U)=CAR (CAR U)
;deps: (NTHD1 NTHD2)

(trw |(car car(u)).(cdr car(u))| nthd4)
;CAR (CAR U).CDR (CAR U)=CAR U

(rw -2 (use * mode: exact) nthd1)
;CAR DOM(U)=CAR (CAR U)
;deps: (NTHD1 NTHD2)

(ci (nthd1 nthd2))
;0<LENGTH U∧ALISTP U⊃CAR DOM(U)=CAR (CAR U)
(label nthd_basecase)

(assume |n<length u∧alistp u⊃car nth(u,n)=nth(dom(u),n)|) 
(label nthd5)

(assume |n'<length(x.u)∧alistp x.u|)
(label nthd6)

(rw *)
;N<LENGTH U∧ALISTP X.U

(derive |car nth(u,n)=nth(dom(u),n)| (* alistfact2 nthd5))
(label nthd7)

(derive |¬atom x∧atom car x∧alistp u| (nthd6 alistfact1))

(trw |nth(dom((car x.cdr x).u),n')| (nuse cons_car_cdr) (open dom) *)
;NTH(DOM((CAR X.CDR X).U),N')=NTH(DOM(U),N)
;deps: (NTHD6)

(rw nthd7 (use * mode: exact direction: reverse))
;CAR NTH(U,N)=NTH(DOM((CAR X.CDR X).U),N')
;deps: (NTHD5 NTHD6)

(trw |car x.cdr x| -3)
;CAR X.CDR X=X
;deps: (INVIL6)

(rw -2 *)
;CAR NTH(U,N)=NTH(DOM(X.U),N')
;deps: (NTHD5 NTHD6)

(ci nthd6)
;N<LENGTH U∧ALISTP X.U⊃CAR NTH(U,N)=NTH(DOM(X.U),N')
;deps: (NTHD5)

(ci nthd5)
;(N<LENGTH U∧ALISTP U⊃CAR NTH(U,N)=NTH(DOM(U),N))⊃
;(N<LENGTH U∧ALISTP X.U⊃CAR NTH(U,N)=NTH(DOM(X.U),N'))
(label nthd_inductioncase)

(ue (phi3 |λu n.n<length u∧alistp u⊃car nth(u,n)=nth(dom(u),n)|) 
    doubleinduction1 nthd_basecase nthd_inductioncase)

(proof nthcdr_dom)
(assume |alistp u⊃nthcdr(dom(u),n)=dom(nthcdr(u,n))|)
(assume |alistp(x.u)|)
(derive |nthcdr(dom u,n)=dom nthcdr(u,n)| (-2 * alistfact2))
(derive |¬atom x∧atom car x∧alistp u| (-2 alistfact1))

(trw |nthcdr(dom((car x.cdr x).u),n')| (use -2 * mode: always)
     (nuse cons_car_cdr) (open dom))
;NTHCDR(DOM((CAR X.CDR X).U),N')=DOM(NTHCDR(U,N))

(rw * -2)
;NTHCDR(DOM(X.U),N')=DOM(NTHCDR(U,N))

(ci -5)
;ALISTP X.U⊃NTHCDR(DOM(X.U),N')=DOM(NTHCDR(U,N))

(ci -7)
;(ALISTP U⊃NTHCDR(DOM(U),N)=DOM(NTHCDR(U,N)))⊃
;(ALISTP X.U⊃NTHCDR(DOM(X.U),N')=DOM(NTHCDR(U,N)))

(ue (phi3 |λu n.alistp u⊃nthcdr(dom u,n)=dom nthcdr(u,n)|) doubleinduction1
    (open dom) *)
;∀U N.ALISTP U⊃NTHCDR(DOM(U),N)=DOM(NTHCDR(U,N))
(label nthcdr_dom)
(proof member_memberdom)
(trw |∀x y.x=y⊃car(x)=car(y)|)
;∀X Y.X=Y⊃CAR X=CAR Y

(ue ((x.|xa.y|)(y.|xa1.y1|)) *)
;XA.Y=XA1.Y1⊃XA=XA1

(ue (chi |λalist. member(xa1.y1,alist)⊃member(xa1,dom alist)|)
    alistinduction (open dom) (use * memberdef normal mode: always))
;∀ALIST.MEMBER(XA1.Y1,ALIST)⊃MEMBER(XA1,DOM(ALIST))
(label member_memberdom)
(proof invimage)


(assume |n≤length alist⊃disjoint(λm.invimage(m,alist),n)|)
(label invimage_indhyp)

(assume |n'≤length alist|)
(label invim0)

(derive |n<length alist| (* less_lesseqsucc))
(label invim1)

(assume |∀n.n<length alist⊃disjoint(λm.setseq(m),n')|)
(label invim2)

(assume |(un(λm.invimage(m,alist),n))(xv)∧(invimage(n,alist))(xv)|)
(label invim3)

(rw invim3 (use unionfact2 ue: ((setseq.|λm.invimage(m,alist)|)(n.n)) mode: exact))
;(∃K.K<N∧(INVIMAGE(K,ALIST))(X))∧(INVIMAGE(N,ALIST))(X)
(label invim4)
;deps: (INVIM3)

(define kw |kw<n∧(invimage(kw,alist))(xv)| invim4)
(label invim5)

(rw invim4 (part 2 (open invimage)))
;(∃K.K<N∧(INVIMAGE(K,ALIST))(xv))∧ATOM xv∧(∃Y.MEMBER(xv.Y,ALIST)∧(SETSEQ(N))(Y))
;deps: (INVIM3)

(define yw1 |member(xv.yw1,alist)∧(setseq n)(yw1)| *)
(label invim6)

(rw invim5 (open invimage))
;KW<N∧ATOM X∧(∃Y.MEMBER(X.Y,ALIST)∧(SETSEQ(KW))(Y))
(label invim7)
;deps: (INVIM3)

(define yw2 |member(xv.yw2,alist)∧(setseq kw)(yw2)| *)
(label invim8)

;yw1 and yw2 are different S-expressions, since they belong to different sets
;of the disjoint sequence setseq

(derive |∃m.m<n∧(setseq m)(yw2)| (invim7 invim8))

(rw * (use unionfact2 ue: ((setseq.setseq)(n.n)) mode: exact direction: reverse))
;(UN(λM.SETSEQ(M),N))(YW2)
(label invim9)

(derive |disjoint(λm.setseq(m),n')| (invim1 invim2))
;deps: (INVIM1 INVIM2)

(rw * (open disjoint disj_pair intersection emptyp))
;DISJOINT(λM.SETSEQ(M),N)∧(∀XV.¬((UN(λM.SETSEQ(M),N))(XV)∧(SETSEQ(N))(XV)))
(label invim10)

(assume |yw1=yw2|)
(label invim11)

(derive |false| (invim6 invim9 invim10 invim11))

(ci invim11)
;¬YW1=YW2
;deps: (INVIM1 INVIM2 INVIM3)
(label invim12)

;therefore xv.yw1 and xv.yw2 are different components of alist

(trw |∀x y.x=y⊃cdr(x)=cdr(y)|)
;∀X Y.X=Y⊃CAR X=CAR Y

(ue ((x.|xv.yw1|)(y.|xv.yw2|)) * invim12)
;¬X.YW1=X.YW2
(label invim13)
;deps: (INVIM1 INVIM2 INVIM3)
 
(derive |∃n.n<length alist∧nth(alist,n)=xv.yw1| (member_nth invim6))
(label invim14)

(derive |∃n.n<length alist∧nth(alist,n)=xv.yw2| (member_nth invim8))
(label invim15)

(define iw |iw<length alist∧nth(alist,iw)=xv.yw1| invim14)
(label invim16)

(define jw |jw<length alist∧nth(alist,jw)=xv.yw2| invim15)
(label invim17)

(assume |iw=jw|)
(label invim18)

(trw |xv.yw1=xv.yw2| (use invim16 invim17 mode: always direction: reverse)
                     (use invim18 mode: exact))
;X.YW1=X.YW2
;deps: (INVIM3 INVIM18)

(derive |false| (* invim13))

(ci invim18)
;¬IW=JW
;deps: (INVIM1 INVIM2 INVIM3)
(label invim19)

;but dom alist is injective

(assume |inj(dom alist)|)
(label invim20)

(rw invim20 (use injdef mode: exact))
;∀N M.N<LENGTH (DOM(ALIST))∧M<LENGTH (DOM(ALIST))∧
;     NTH(DOM(ALIST),N)=NTH(DOM(ALIST),M)⊃N=M
;deps: (INVIM20)

(derive |iw<length dom(alist)∧jw<length dom(alist)| (invim16 invim17 domlength))

(derive |nth(dom(alist),iw)=nth(dom(alist),jw)⊃iw=jw| (-2 *))
(label invim21)

(ue ((u.alist)(n.iw)) nth_dom (use invim16 mode: always))
;X=NTH(DOM(ALIST),IW)
;deps: (INVIM3)

(ue ((u.alist)(n.jw)) nth_dom (use invim17 mode: always))
;X=NTH(DOM(ALIST),JW)
;deps: (INVIM3)

(rw invim21 (use * -2 mode: exact direction: reverse))
;IW=JW
;deps: (INVIM3 INVIM20)

(rw * invim19)
;FALSE
;deps: (INVIM1 INVIM2 INVIM3 INVIM20)

(ci invim3)
;¬((UN(λM.INVIMAGE(M,ALIST),N))(X)∧(INVIMAGE(N,ALIST))(X))
;deps: (INVIM1 INVIM2 INVIM20)
(label invim22)

(trw |n≤length alist| (open lesseq) invim1)
(derive |disjoint(λm.invimage(m,alist),n)| (* invimage_indhyp))
(label invim23)
 
(trw |disjoint(λm.invimage(m,alist),n')| 
     (open disjoint disj_pair intersection emptyp) invim22 invim23)
;DISJOINT(λM.INVIMAGE(M,ALIST),N')
;deps: (INVIMAGE_INDHYP INVIM0 INVIM2 INVIM20)

(ci invim0)
;N'≤LENGTH ALIST⊃DISJOINT(λM.INVIMAGE(M,ALIST),N')
;deps: (INVIMAGE_INDHYP INVIM2 INVIM20)

(ci invimage_indhyp)
;(N≤LENGTH ALIST⊃DISJOINT(λM.INVIMAGE(M,ALIST),N))⊃
;(N'≤LENGTH ALIST⊃DISJOINT(λM.INVIMAGE(M,ALIST),N'))
;deps: (INVIM2 INVIM20)

(ue (a |λn.n≤length alist⊃disjoint(λm.invimage(m,alist),n)|) proof_by_induction
    * (part 1#1(open disjoint)))
;∀N.N≤LENGTH ALIST⊃DISJOINT(λM.INVIMAGE(M,ALIST),N)
;deps: (INVIM2 INVIM20)

(ci (invim2 invim20))
;(∀N.N<LENGTH ALIST⊃DISJOINT(λM.SETSEQ(M),N'))∧INJ(DOM(ALIST))⊃
;(∀N.N≤LENGTH ALIST⊃DISJOINT(λM.INVIMAGE(M,ALIST),N))


(proof double_alistinduction)
(axiom |∀u n.alistp u∧n<length u⊃cdr nth(u,n)=nth(range(u),n)|)
(label nth_range)

(axiom |∀u n.alistp u∧n<length u⊃car nth(u,n)=nth(dom(u),n)|)
(label nth_dom)

(assume |∀alist n xa y.chi3(nil,n)∧chi3(alist,0)∧
                       (chi3(alist,n)⊃chi3((xa.y).alist,n'))|)
(label dalistassume)
                                                                       
(ue (chi |λalist.∀n.chi3(alist,n)|) alistinduction
    (use dalistassume) 
    (use proof_by_induction ue: ((a.|λn.chi3((xa.y).alist,n)|)) ))
;∀ALIST N.CHI3(ALIST,N)
;deps: (DALISTASSUME)
 
(ci dalistassume)
;(∀ALIST N XA Y.CHI3(NIL,N)∧CHI3(ALIST,0)∧
;               (CHI3(ALIST,N)⊃CHI3((XA.Y).ALIST,N')))⊃(∀ALIST N.CHI3(ALIST,N))
(label double_alistinduction1)


(proof appalist_nth)

(ue (chi |λalist.uniqueness(dom(alist))⊃
                 cdr assoc(car dom(alist),alist)=car range(alist)|)
    alistinduction (open uniqueness assoc dom range))
;∀ALIST.UNIQUENESS(DOM(ALIST))⊃CDR ASSOC(CAR DOM(ALIST),ALIST)=CAR RANGE(ALIST)
(label a_n_base)

;a negative rewriter for the inductive step

(assume |n<length dom(alist)∧xa=nth(dom alist,n)|)
(label a_n1)

(trw |member(xa,dom alist)| nthmember (use * mode: always))
;MEMBER(XA,DOM(ALIST))
;deps: (A_N1)

(ci a_n1)
;N<LENGTH (DOM(ALIST))∧XA=NTH(DOM(ALIST),N)⊃MEMBER(XA,DOM(ALIST))
(label a_n2)

(assume |¬member(xa,dom alist)|)
(label a_n3)

(derive |∀n.n<length dom(alist)⊃nth(dom alist,n)≠xa| (* a_n2))
;deps: (A_N3)

(ci a_n3)
;¬MEMBER(XA,DOM(ALIST))⊃(∀N.N<LENGTH (DOM(ALIST))⊃¬NTH(DOM(ALIST),N)=XA)
(label a_n4)

;we are ready 

(ue (chi3 |λalist n.uniqueness dom(alist) ∧ n<length dom(alist) ⊃ 
                    appalist(nth(dom alist,n),alist)= nth(range alist,n)|)
    double_alistinduction1 atom_nth a_n_base 
    (part 1 (open appalist assoc dom range uniqueness))(use a_n4 mode: always))
;∀ALIST N.UNIQUENESS(DOM(ALIST))∧N<LENGTH (DOM(ALIST))⊃
;         APPALIST(NTH(DOM(ALIST),N),ALIST)=NTH(RANGE(ALIST),N)